In general, a system development process includes a requirements development stage, a design and development stage and a verification stage. A requirement may be characterized as a documented need of how a particular product or service should perform. More particularly, a requirement may be referred to as a statement that identifies the necessary functionalities, attributes, capabilities, characteristics or qualities of a system. Requirements in the form of a requirements specification are used as inputs into the design stages of a system development process to design what elements and functions are necessary for a particular system.
Requirement specifications can be expressed using a variety of languages. These languages may be graphical or textual in nature and may include, without limitation, transition systems (e.g., state machines), event sequence charts (e.g., scenario or sequence diagrams) and structured English language. The system is implemented using software or hardware or both, often using interfaces implemented using sensors to sense the environment (including the user) inputs and actuators to control the hardware. In complex systems, particularly those in which safety is a primary concern, exhaustive testing and verification of the system, is required to ensure that the behavior of the system satisfies the requirements specification of the system.
A common approach to testing and verifying system is formal verification. Broadly, formal verification is the process of proving or disproving the correctness of intended algorithms underlying a system with respect to a formal specification (also referred to as a property), using a class of state space exploration methods. One formal verification approach is model checking, which is an automatic, systematic, exhaustive exploration of the behaviors of the model. Usually, this includes exploring all states and transitions in the model by using smart and domain-specific abstraction techniques to consider whole groups of states in a single operation and reduce computing time. Implementation techniques include state space enumeration, symbolic state space enumeration, abstract interpretation, symbolic simulation and abstraction refinement. The properties to be verified are often described in a temporal logic, such as linear temporal logic (LTL) or computational tree logic (CTL).
Known formal verification methods are normally applicable only to the models of the system at the design stage, or to the software portion of the systems. Although theoretically possible, models for entire systems can be impossible to implement, or at best, be extremely large so that existing formal methods techniques cannot scale to tackle the resulting large state space. Therefore, testing using simulation of the system is the only way of verifying the system against its requirements specification. However, since the test cases (test inputs to the system and the desired outputs) are written by testers, they usually test only simple specifications. This is because writing test cases for complex temporal specifications is error-prone. In addition, checking the simulation runs against the desired outputs according to complex temporal specifications is also time consuming and error-prone. Thus, there is a need to provide a system and method for automatic formal verification of an executable system that is scalable to any size system.